A Kripke structure is a variation of nondeterministic automaton proposed by Saul Kripke [1], used in model checking to represent the behavior of a system. It is a simple abstract machine (a mathematical object) to capture the idea of a computing machine, without adding unnecessary complexities. It is basically a graph whose nodes represent the reachable states of the system and whose edges represent state transitions. A labeling function maps each node to a set of properties that hold in the corresponding state. Temporal logics are traditionally interpreted in terms of Kripke structures.
Contents |
Let AP be a set of atomic propositions, i.e. boolean expressions over variables, constants and predicate symbols. Clarke et al.[2] define a Kripke structure over AP is a 4-tuple M = (S, I, R, L) consisting of
Since R is left-total, it is always possible to construct an infinite path through the Kripke structure. A deadlock state can be modeled by a single outgoing edge back to itself. The labeling function L defines for each state s ∈ S the set L(s) of all atomic propositions that are valid in s.
A path of the structure M is a sequence of states ρ = s1,s2,s3,... such that for each i > 0, si+1 = R(si). The word on the path ρ is sequence of sets of the atomic propositions w=L(s1),L(s2),L(s3),..., which is an ω-word over alphabet 2AP.
With this definition, a Kripke structure may be identified with a Moore machine with a singleton input alphabet, and with the output function being its labeling function.[3]
Let the set of atomic propositions AP = {p,q}. p and q can model arbitrary boolean properties of the system that the kripke structure is modelling.
The figure at right illustrates a kripke structure M=(S, I, R, L), where
M may produce a path ρ = s1,s2,s1,s2,s3,s3,s3,... and w = {p,q},{q},{p,q},{q},{p},{p},{p},... is the execution word over the path ρ. M can produce execution words belonging to the language ({p,q}{q})*({p})ω∪({p,q}{q})ω.
Although this terminology is widespread in the model checking community, some textbooks on model checking do not define "Kripke structure" in this extended way (or at all in fact), but simply use the concept of a (labelled) transition system, which additionally has a set Act of actions, and the transition relation is defined as a subset of S × Act × S, which they additionally extend to include a set of atomic propositions and a labeling function for the states as well (L as defined above.) In this approach, the binary relation obtained by abstracting away the action labels is called a state graph.[4]
Clarke et al. redefine a Kripke structure as a set of transitions (instead of just one), which is equivalent to the labeled transitions above, when they define the semantics of modal μ-calculus.[5]